Require coherence of supertrait associated item bounds for dyn-compability - #158915
Require coherence of supertrait associated item bounds for dyn-compability#158915theemathas wants to merge 2 commits into
Conversation
rustbot
added
S-waiting-on-review
|
I'm unsure of what to do with the now-failing tests. I'm also rather unsure of my code in general. Please be careful with the review to make sure I didn't do anything stupid. Thank you. |
theemathas
added
needs-fcp
4d67fa1 to
256670e
Compare
|
r? types |
rustbot
added
the
T-types
| // Note that we discard any obligations we get here. | ||
| // We don't care about proving them. | ||
| // | ||
| // If this call returns an Err, then the two sets of generic args | ||
| // can't possibly be instantiated with the same concrete types. | ||
| // So, we return true from the function |
There was a problem hiding this comment.
you could do the proper coherence thing and actually use an ObligationCtxt and try_evaluate
makes slightly more compile
There was a problem hiding this comment.
Sorry, but I don't understand what you mean. What is an ObligationCtxt, and how does using it cause more code to compile?
| ) -> bool { | ||
| // We syntactically compare the two terms. If they're equal, then | ||
| // they do not conflict with each other. | ||
| // FIXME: This is an overly strict definition of equality. Could this be done better? |
There was a problem hiding this comment.
if we check for equality in the param_env of the trait and prove nested obligations + regions, this should be correct?
as in, what we prove here is
for<trait_params, trait-where-clauses> assoc1 == assoc2
=> assoc1_term == assoc2_term
and we under-approximate by
for<trait_params, trait-where-clauses> assoc1 != assoc2
OR
for<trait_params, trait-where-clauses> assoc1term == assoc2term
which we impl as
!exists<trait_params, trait-where-clauses> assoc1 == assoc2
OR
for<trait_params, trait-where-clauses> assoc1term == assoc2term
so to make this check more permissive, you could check the where-clauses of the trait in the exists check :>
There was a problem hiding this comment.
What's a nested obligation? What's a nested region? What's "the param_env of the trait"? What does it mean to "check" the where clauses of a trait?
|
after that, we should do a crater run 😁 |
|
@rustbot author |
rustbot
added
S-waiting-on-author
|
Reminder, once the PR becomes ready for a review, use |
This comment has been minimized.
This comment has been minimized.
…ics. See rust-lang#154662 These tests will be fixed in a subsequent commit.
256670e to
4adf718
Compare
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
…ility Fixes rust-lang#154662 In a `dyn` type, if multiple bounds are specified via supertraits for the same associated item, then we previously accepted them if the relevant trait's generics are different, even if the bounds conflict. This was unsound, since those generics could end up being instantiated with identical concrete types, causing the `dyn` type to have two different "values" for the same bound. Thus, if a trait has multiple supertrait bounds for the same associated item, we check whether those bounds are coherent, similarly to how we check for overlap between impls (i.e., we check if the generics could be instantiated to be the same while the "values" of the bounds are different). If the bounds are incoherent, then we consider the trait to be dyn-incompatible.
4adf718 to
97592bc
Compare
|
I decided to ask an LLM for assistance with understanding how the trait solver API works, and with double-checking my code for any glaring issues. I still wrote all code manually. In particular, the LLM did the following:
I claim full responsibility of all code in this PR. |
| // Now that we've constrained the two projections to be on the same thing, | ||
| // we check whether the two terms are necessarily equal to each other. | ||
| // If they are, then the two projections are coherent. | ||
| plug_infer_with_placeholders(&infcx, ty::UniverseIndex::ROOT, (proj_1, proj_2)); | ||
| let ocx = ObligationCtxt::new(&infcx); | ||
| ocx.eq(&ObligationCause::dummy(), param_env, proj_1.term, proj_2.term).is_ok() | ||
| && ocx.evaluate_obligations_error_on_ambiguity().no_errors() | ||
| && ocx.resolve_regions(CRATE_DEF_ID, param_env, []).is_empty() | ||
| } |
There was a problem hiding this comment.
The LLM, in reviewing my code, told me that I have to instantiate the param_env with trait_args here. However, I should not do this instantiation in the can_equate_generics computation. Is the LLM right here? I don't understand at all what this does.
There was a problem hiding this comment.
This test is currently the only pre-existing test that this PR breaks. What should be done about this test?
|
Is this PR ready for a crater run? @rustbot ready |
rustbot
added
S-waiting-on-review
4 participants
This PR is an alternative to #157710. However, unlike that PR, this PR does not address #150936.
Fixes #154662
In a
dyntype, if multiple bounds are specified via supertraits for the same associated item, then we previously accepted them if the relevant trait's generics are different, even if the bounds conflict.This was unsound, since those generics could end up being instantiated with identical concrete types, causing the
dyntype to have two different "values" for the same bound.Thus, if a trait has multiple supertrait bounds for the same associated item, we check whether those bounds are coherent, similarly to how we check for overlap between impls (i.e., we check if the generics could be instantiated to be the same while the "values" of the bounds are different). If the bounds are incoherent, then we consider the trait to be dyn-incompatible.
r? @fmease